○○ as ○○ - pogi-log

○○ as ○○

○○を○○と見なすという見方

カリー＝ハワード対応やPropositions as Typesは○○ as ○○が多く含まれている

Propositions as some Types

Algebras as Types

Coalgebras as Types

Categories as Types

Logical Relations as Types[Jonathan2020]

カリー＝ハワード対応

formulae as types

proof as programs

proofs as terms(PAT)

Propositions as Types

ハイパードクトリン

Logical Relation as Category

Homotopy Type Theory(HoTT)

Types as Spaces

メモ

集合論・圏論 vs. 型理論 - 檜山正幸のキマイラ飼育記 (はてなBlog)

[Jonathan2020] 【2010.08599】 Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

『Introduction to Homotopy Type Theory』